; benchmark generated from python API
(set-info :status unknown)
(declare-fun back_top_feasible () Bool)
(declare-fun back_top_kid_0_feasible () Bool)
(declare-fun back_top_kid_0_width () Real)
(declare-fun back_top_kid_0_hight () Real)
(declare-fun back_top_hight () Real)
(declare-fun back_top_kid_0_y () Real)
(declare-fun back_top_width () Real)
(declare-fun back_top_kid_0_x () Real)
(assert
 (let (($x2000 (= back_top_kid_0_width 100.0)))
 (let (($x1999 (= (+ (- back_top_kid_0_y back_top_hight) back_top_kid_0_hight) (- 10.0))))
 (let (($x1996 (= back_top_kid_0_y 10.0)))
 (let (($x1995 (>= (- (+ (- back_top_kid_0_y) back_top_hight) back_top_kid_0_hight) 10.0)))
 (let (($x1991 (>= back_top_kid_0_y 10.0)))
 (let (($x1990 (>= (- (+ (- back_top_kid_0_x) back_top_width) back_top_kid_0_width) 10.0)))
 (let (($x1986 (>= back_top_kid_0_x 10.0)))
 (let ((?x1984 (+ (- (* 2.0 back_top_kid_0_x) back_top_width) back_top_kid_0_width)))
 (let (($x1985 (= ?x1984 0.0)))
 (let (($x1981 (>= back_top_kid_0_hight 0.0)))
 (let (($x1980 (>= back_top_kid_0_width 0.0)))
 (let (($x1979 (>= back_top_kid_0_y 0.0)))
 (let (($x1978 (>= back_top_kid_0_x 0.0)))
 (and $x1978 $x1979 $x1980 $x1981 $x1985 $x1986 $x1990 $x1991 $x1995 $x1996 $x1999 $x2000 back_top_kid_0_feasible back_top_feasible)))))))))))))))
(check-sat)

